/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package simhya.modelchecking.mtl;


/**
 *
 * @author Luca
 */
public class MTLglobally  extends MTLmodalNode {
    
    public MTLglobally(MTLnode child) {
        super(new ParametricInterval());
        super.setChild(child);
        child.setParent(this);
    }

    public MTLglobally(ParametricInterval interval, MTLnode child) {
        super(interval);
        super.setChild(child);
        child.setParent(this);
    }
    
    @Override
    public String toFormulaTree(int depth) {
        String s = "";
        for (int i=0;i<depth;i++)
            s += "   ";
        s += "Globally " + parametricInterval.toString() + "\n";
        return s + super.toFormulaTree(depth);
    }
    
    /*
     * Here we check in fact the formula eventually not phi, and negate the result
     */
    
     @Override
    boolean checkGoal(int j) {
        if (j < this.traceLength) 
            return !child.truthValue[j];
        else return true; //not sure of this last point
    }

    @Override
    boolean checkSafe(int i) {
        return true;
    }

    @Override
    void setBad(int i) {
        this.truthValue[i] = true;
    }

    @Override
    void setOk(int i) {
        this.truthValue[i] = false;
    }
    
}
